Left Termination proof of /tmp/tmppG

Left Termination of the query pattern zebra_in_7(a, a, a, a, a, a, a) w.r.t. the given Prolog program could successfully be proven:

↳ Prolog

  ↳ PrologToPiTRSProof

Clauses:

zebra(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) :- ','(eq(Englishman, Red), ','(eq(Spaniard, Dog), ','(eq(Green, Coffee), ','(eq(Ukrainian, Tea), ','(to_the_right(Green, Ivory), ','(eq(Winston, Snails), ','(eq(Kool, Yellow), ','(eq(Milk, third), ','(eq(Norwegian, first), ','(next_to(Fox, Chesterfield), ','(next_to(Horse, Kool), ','(eq(Lucky, Juice), ','(eq(Japanese, Parliament), ','(next_to(Norwegian, Blue), ','(houses(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))), ','(houses(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))), ','(houses(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))), ','(houses(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))), houses(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))))))))))))))))))).
houses(Prop) :- domain(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))).
domain([], X).
domain(.(X, Rest), Domain) :- ','(select(X, Domain, NewDomain), domain(Rest, NewDomain)).
select(X, .(X, R), R).
select(X, .(Y, R), .(Y, Rest)) :- select(X, R, Rest).
next_to(fifth, fourth).
next_to(fourth, fifth).
next_to(fourth, third).
next_to(third, fourth).
next_to(third, second).
next_to(second, third).
next_to(second, first).
next_to(first, second).
to_the_right(fifth, fourth).
to_the_right(fourth, third).
to_the_right(third, second).
to_the_right(second, first).
eq(X, X).

Queries:

zebra(a,a,a,a,a,a,a).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

zebra_in(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in(Englishman, Red))
eq_in(X, X) → eq_out(X, X)
U1(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out(Englishman, Red)) → U2(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in(Spaniard, Dog))
U2(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out(Spaniard, Dog)) → U3(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in(Green, Coffee))
U3(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out(Green, Coffee)) → U4(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in(Ukrainian, Tea))
U4(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out(Ukrainian, Tea)) → U5(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in(Green, Ivory))
to_the_right_in(second, first) → to_the_right_out(second, first)
to_the_right_in(third, second) → to_the_right_out(third, second)
to_the_right_in(fourth, third) → to_the_right_out(fourth, third)
to_the_right_in(fifth, fourth) → to_the_right_out(fifth, fourth)
U5(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out(Green, Ivory)) → U6(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in(Winston, Snails))
U6(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out(Winston, Snails)) → U7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in(Kool, Yellow))
U7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out(Kool, Yellow)) → U8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in(Milk, third))
U8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out(Milk, third)) → U9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in(Norwegian, first))
U9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out(Norwegian, first)) → U10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in(Fox, Chesterfield))
next_to_in(first, second) → next_to_out(first, second)
next_to_in(second, first) → next_to_out(second, first)
next_to_in(second, third) → next_to_out(second, third)
next_to_in(third, second) → next_to_out(third, second)
next_to_in(third, fourth) → next_to_out(third, fourth)
next_to_in(fourth, third) → next_to_out(fourth, third)
next_to_in(fourth, fifth) → next_to_out(fourth, fifth)
next_to_in(fifth, fourth) → next_to_out(fifth, fourth)
U10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out(Fox, Chesterfield)) → U11(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in(Horse, Kool))
U11(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out(Horse, Kool)) → U12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in(Lucky, Juice))
U12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out(Lucky, Juice)) → U13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in(Japanese, Parliament))
U13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out(Japanese, Parliament)) → U14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in(Norwegian, Blue))
U14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out(Norwegian, Blue)) → U15(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in(Prop) → U20(Prop, domain_in(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in(.(X, Rest), Domain) → U21(X, Rest, Domain, select_in(X, Domain, NewDomain))
select_in(X, .(Y, R), .(Y, Rest)) → U23(X, Y, R, Rest, select_in(X, R, Rest))
select_in(X, .(X, R), R) → select_out(X, .(X, R), R)
U23(X, Y, R, Rest, select_out(X, R, Rest)) → select_out(X, .(Y, R), .(Y, Rest))
U21(X, Rest, Domain, select_out(X, Domain, NewDomain)) → U22(X, Rest, Domain, domain_in(Rest, NewDomain))
domain_in([], X) → domain_out([], X)
U22(X, Rest, Domain, domain_out(Rest, NewDomain)) → domain_out(.(X, Rest), Domain)
U20(Prop, domain_out(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out(Prop)
U15(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

zebra_in(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in(Englishman, Red))
eq_in(X, X) → eq_out(X, X)
U1(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out(Englishman, Red)) → U2(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in(Spaniard, Dog))
U2(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out(Spaniard, Dog)) → U3(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in(Green, Coffee))
U3(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out(Green, Coffee)) → U4(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in(Ukrainian, Tea))
U4(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out(Ukrainian, Tea)) → U5(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in(Green, Ivory))
to_the_right_in(second, first) → to_the_right_out(second, first)
to_the_right_in(third, second) → to_the_right_out(third, second)
to_the_right_in(fourth, third) → to_the_right_out(fourth, third)
to_the_right_in(fifth, fourth) → to_the_right_out(fifth, fourth)
U5(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out(Green, Ivory)) → U6(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in(Winston, Snails))
U6(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out(Winston, Snails)) → U7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in(Kool, Yellow))
U7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out(Kool, Yellow)) → U8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in(Milk, third))
U8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out(Milk, third)) → U9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in(Norwegian, first))
U9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out(Norwegian, first)) → U10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in(Fox, Chesterfield))
next_to_in(first, second) → next_to_out(first, second)
next_to_in(second, first) → next_to_out(second, first)
next_to_in(second, third) → next_to_out(second, third)
next_to_in(third, second) → next_to_out(third, second)
next_to_in(third, fourth) → next_to_out(third, fourth)
next_to_in(fourth, third) → next_to_out(fourth, third)
next_to_in(fourth, fifth) → next_to_out(fourth, fifth)
next_to_in(fifth, fourth) → next_to_out(fifth, fourth)
U10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out(Fox, Chesterfield)) → U11(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in(Horse, Kool))
U11(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out(Horse, Kool)) → U12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in(Lucky, Juice))
U12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out(Lucky, Juice)) → U13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in(Japanese, Parliament))
U13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out(Japanese, Parliament)) → U14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in(Norwegian, Blue))
U14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out(Norwegian, Blue)) → U15(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in(Prop) → U20(Prop, domain_in(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in(.(X, Rest), Domain) → U21(X, Rest, Domain, select_in(X, Domain, NewDomain))
select_in(X, .(Y, R), .(Y, Rest)) → U23(X, Y, R, Rest, select_in(X, R, Rest))
select_in(X, .(X, R), R) → select_out(X, .(X, R), R)
U23(X, Y, R, Rest, select_out(X, R, Rest)) → select_out(X, .(Y, R), .(Y, Rest))
U21(X, Rest, Domain, select_out(X, Domain, NewDomain)) → U22(X, Rest, Domain, domain_in(Rest, NewDomain))
domain_in([], X) → domain_out([], X)
U22(X, Rest, Domain, domain_out(Rest, NewDomain)) → domain_out(.(X, Rest), Domain)
U20(Prop, domain_out(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out(Prop)
U15(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

ZEBRA_IN(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in(Englishman, Red))
ZEBRA_IN(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → EQ_IN(Englishman, Red)
U1¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out(Englishman, Red)) → U2¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in(Spaniard, Dog))
U1¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out(Englishman, Red)) → EQ_IN(Spaniard, Dog)
U2¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out(Spaniard, Dog)) → U3¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in(Green, Coffee))
U2¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out(Spaniard, Dog)) → EQ_IN(Green, Coffee)
U3¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out(Green, Coffee)) → U4¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in(Ukrainian, Tea))
U3¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out(Green, Coffee)) → EQ_IN(Ukrainian, Tea)
U4¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out(Ukrainian, Tea)) → U5¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in(Green, Ivory))
U4¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out(Ukrainian, Tea)) → TO_THE_RIGHT_IN(Green, Ivory)
U5¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out(Green, Ivory)) → U6¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in(Winston, Snails))
U5¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out(Green, Ivory)) → EQ_IN(Winston, Snails)
U6¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out(Winston, Snails)) → U7¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in(Kool, Yellow))
U6¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out(Winston, Snails)) → EQ_IN(Kool, Yellow)
U7¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out(Kool, Yellow)) → U8¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in(Milk, third))
U7¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out(Kool, Yellow)) → EQ_IN(Milk, third)
U8¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out(Milk, third)) → U9¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in(Norwegian, first))
U8¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out(Milk, third)) → EQ_IN(Norwegian, first)
U9¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out(Norwegian, first)) → U10¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in(Fox, Chesterfield))
U9¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out(Norwegian, first)) → NEXT_TO_IN(Fox, Chesterfield)
U10¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out(Fox, Chesterfield)) → U11¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in(Horse, Kool))
U10¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out(Fox, Chesterfield)) → NEXT_TO_IN(Horse, Kool)
U11¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out(Horse, Kool)) → U12¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in(Lucky, Juice))
U11¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out(Horse, Kool)) → EQ_IN(Lucky, Juice)
U12¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out(Lucky, Juice)) → U13¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in(Japanese, Parliament))
U12¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out(Lucky, Juice)) → EQ_IN(Japanese, Parliament)
U13¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out(Japanese, Parliament)) → U14¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in(Norwegian, Blue))
U13¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out(Japanese, Parliament)) → NEXT_TO_IN(Norwegian, Blue)
U14¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out(Norwegian, Blue)) → U15¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
U14¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out(Norwegian, Blue)) → HOUSES_IN(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))
HOUSES_IN(Prop) → U20¹(Prop, domain_in(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
HOUSES_IN(Prop) → DOMAIN_IN(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))
DOMAIN_IN(.(X, Rest), Domain) → U21¹(X, Rest, Domain, select_in(X, Domain, NewDomain))
DOMAIN_IN(.(X, Rest), Domain) → SELECT_IN(X, Domain, NewDomain)
SELECT_IN(X, .(Y, R), .(Y, Rest)) → U23¹(X, Y, R, Rest, select_in(X, R, Rest))
SELECT_IN(X, .(Y, R), .(Y, Rest)) → SELECT_IN(X, R, Rest)
U21¹(X, Rest, Domain, select_out(X, Domain, NewDomain)) → U22¹(X, Rest, Domain, domain_in(Rest, NewDomain))
U21¹(X, Rest, Domain, select_out(X, Domain, NewDomain)) → DOMAIN_IN(Rest, NewDomain)
U15¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U15¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → HOUSES_IN(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))
U16¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U16¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → HOUSES_IN(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))
U17¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U17¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → HOUSES_IN(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))
U18¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U18¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → HOUSES_IN(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))

The TRS R consists of the following rules:

zebra_in(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in(Englishman, Red))
eq_in(X, X) → eq_out(X, X)
U1(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out(Englishman, Red)) → U2(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in(Spaniard, Dog))
U2(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out(Spaniard, Dog)) → U3(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in(Green, Coffee))
U3(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out(Green, Coffee)) → U4(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in(Ukrainian, Tea))
U4(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out(Ukrainian, Tea)) → U5(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in(Green, Ivory))
to_the_right_in(second, first) → to_the_right_out(second, first)
to_the_right_in(third, second) → to_the_right_out(third, second)
to_the_right_in(fourth, third) → to_the_right_out(fourth, third)
to_the_right_in(fifth, fourth) → to_the_right_out(fifth, fourth)
U5(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out(Green, Ivory)) → U6(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in(Winston, Snails))
U6(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out(Winston, Snails)) → U7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in(Kool, Yellow))
U7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out(Kool, Yellow)) → U8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in(Milk, third))
U8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out(Milk, third)) → U9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in(Norwegian, first))
U9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out(Norwegian, first)) → U10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in(Fox, Chesterfield))
next_to_in(first, second) → next_to_out(first, second)
next_to_in(second, first) → next_to_out(second, first)
next_to_in(second, third) → next_to_out(second, third)
next_to_in(third, second) → next_to_out(third, second)
next_to_in(third, fourth) → next_to_out(third, fourth)
next_to_in(fourth, third) → next_to_out(fourth, third)
next_to_in(fourth, fifth) → next_to_out(fourth, fifth)
next_to_in(fifth, fourth) → next_to_out(fifth, fourth)
U10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out(Fox, Chesterfield)) → U11(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in(Horse, Kool))
U11(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out(Horse, Kool)) → U12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in(Lucky, Juice))
U12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out(Lucky, Juice)) → U13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in(Japanese, Parliament))
U13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out(Japanese, Parliament)) → U14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in(Norwegian, Blue))
U14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out(Norwegian, Blue)) → U15(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in(Prop) → U20(Prop, domain_in(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in(.(X, Rest), Domain) → U21(X, Rest, Domain, select_in(X, Domain, NewDomain))
select_in(X, .(Y, R), .(Y, Rest)) → U23(X, Y, R, Rest, select_in(X, R, Rest))
select_in(X, .(X, R), R) → select_out(X, .(X, R), R)
U23(X, Y, R, Rest, select_out(X, R, Rest)) → select_out(X, .(Y, R), .(Y, Rest))
U21(X, Rest, Domain, select_out(X, Domain, NewDomain)) → U22(X, Rest, Domain, domain_in(Rest, NewDomain))
domain_in([], X) → domain_out([], X)
U22(X, Rest, Domain, domain_out(Rest, NewDomain)) → domain_out(.(X, Rest), Domain)
U20(Prop, domain_out(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out(Prop)
U15(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

The argument filtering Pi contains the following mapping:
zebra_in(x1, x2, x3, x4, x5, x6, x7) = zebra_in
U1(x1, x2, x3, x4, x5, x6, x7, x8) = U1(x8)
eq_in(x1, x2) = eq_in
eq_out(x1, x2) = eq_out
U2(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U2(x9)
U3(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = U3(x10)
U4(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = U4(x12)
U5(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U5(x13)
to_the_right_in(x1, x2) = to_the_right_in
second = second
first = first
to_the_right_out(x1, x2) = to_the_right_out(x1, x2)
third = third
fourth = fourth
fifth = fifth
U6(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) = U6(x14)
U7(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = U7(x16)
U8(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18) = U8(x18)
U9(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U9(x19)
U10(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U10(x19)
next_to_in(x1, x2) = next_to_in
next_to_out(x1, x2) = next_to_out(x1, x2)
U11(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U11(x21)
U12(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22) = U12(x22)
U13(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24) = U13(x24)
U14(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25) = U14(x25)
U15(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U15(x5, x21)
houses_in(x1) = houses_in(x1)
.(x1, x2) = .(x2)
[] = []
U20(x1, x2) = U20(x2)
domain_in(x1, x2) = domain_in(x1, x2)
U21(x1, x2, x3, x4) = U21(x2, x4)
select_in(x1, x2, x3) = select_in(x2)
U23(x1, x2, x3, x4, x5) = U23(x5)
select_out(x1, x2, x3) = select_out(x3)
U22(x1, x2, x3, x4) = U22(x4)
domain_out(x1, x2) = domain_out
houses_out(x1) = houses_out
U16(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U16(x5, x21)
U17(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U17(x5, x17)
U18(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = U18(x5, x12)
U19(x1, x2, x3, x4, x5, x6, x7, x8) = U19(x5, x8)
zebra_out(x1, x2, x3, x4, x5, x6, x7) = zebra_out(x5)
U15¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U15¹(x5, x21)
U20¹(x1, x2) = U20¹(x2)
DOMAIN_IN(x1, x2) = DOMAIN_IN(x1, x2)
U18¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = U18¹(x5, x12)
SELECT_IN(x1, x2, x3) = SELECT_IN(x2)
U22¹(x1, x2, x3, x4) = U22¹(x4)
EQ_IN(x1, x2) = EQ_IN
HOUSES_IN(x1) = HOUSES_IN(x1)
U12¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22) = U12¹(x22)
U6¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) = U6¹(x14)
U2¹(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U2¹(x9)
U19¹(x1, x2, x3, x4, x5, x6, x7, x8) = U19¹(x5, x8)
NEXT_TO_IN(x1, x2) = NEXT_TO_IN
U17¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17) = U17¹(x5, x17)
U13¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24) = U13¹(x24)
TO_THE_RIGHT_IN(x1, x2) = TO_THE_RIGHT_IN
U5¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U5¹(x13)
ZEBRA_IN(x1, x2, x3, x4, x5, x6, x7) = ZEBRA_IN
U14¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25) = U14¹(x25)
U7¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16) = U7¹(x16)
U23¹(x1, x2, x3, x4, x5) = U23¹(x5)
U10¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U10¹(x19)
U4¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) = U4¹(x12)
U3¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = U3¹(x10)
U1¹(x1, x2, x3, x4, x5, x6, x7, x8) = U1¹(x8)
U21¹(x1, x2, x3, x4) = U21¹(x2, x4)
U8¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18) = U8¹(x18)
U9¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19) = U9¹(x19)
U16¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U16¹(x5, x21)
U11¹(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21) = U11¹(x21)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

ZEBRA_IN(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in(Englishman, Red))
ZEBRA_IN(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → EQ_IN(Englishman, Red)
U1¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out(Englishman, Red)) → U2¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in(Spaniard, Dog))
U1¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out(Englishman, Red)) → EQ_IN(Spaniard, Dog)
U2¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out(Spaniard, Dog)) → U3¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in(Green, Coffee))
U2¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out(Spaniard, Dog)) → EQ_IN(Green, Coffee)
U3¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out(Green, Coffee)) → U4¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in(Ukrainian, Tea))
U3¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out(Green, Coffee)) → EQ_IN(Ukrainian, Tea)
U4¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out(Ukrainian, Tea)) → U5¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in(Green, Ivory))
U4¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out(Ukrainian, Tea)) → TO_THE_RIGHT_IN(Green, Ivory)
U5¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out(Green, Ivory)) → U6¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in(Winston, Snails))
U5¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out(Green, Ivory)) → EQ_IN(Winston, Snails)
U6¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out(Winston, Snails)) → U7¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in(Kool, Yellow))
U6¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out(Winston, Snails)) → EQ_IN(Kool, Yellow)
U7¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out(Kool, Yellow)) → U8¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in(Milk, third))
U7¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out(Kool, Yellow)) → EQ_IN(Milk, third)
U8¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out(Milk, third)) → U9¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in(Norwegian, first))
U8¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out(Milk, third)) → EQ_IN(Norwegian, first)
U9¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out(Norwegian, first)) → U10¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in(Fox, Chesterfield))
U9¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out(Norwegian, first)) → NEXT_TO_IN(Fox, Chesterfield)
U10¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out(Fox, Chesterfield)) → U11¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in(Horse, Kool))
U10¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out(Fox, Chesterfield)) → NEXT_TO_IN(Horse, Kool)
U11¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out(Horse, Kool)) → U12¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in(Lucky, Juice))
U11¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out(Horse, Kool)) → EQ_IN(Lucky, Juice)
U12¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out(Lucky, Juice)) → U13¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in(Japanese, Parliament))
U12¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out(Lucky, Juice)) → EQ_IN(Japanese, Parliament)
U13¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out(Japanese, Parliament)) → U14¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in(Norwegian, Blue))
U13¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out(Japanese, Parliament)) → NEXT_TO_IN(Norwegian, Blue)
U14¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out(Norwegian, Blue)) → U15¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
U14¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out(Norwegian, Blue)) → HOUSES_IN(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))
HOUSES_IN(Prop) → U20¹(Prop, domain_in(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
HOUSES_IN(Prop) → DOMAIN_IN(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))
DOMAIN_IN(.(X, Rest), Domain) → U21¹(X, Rest, Domain, select_in(X, Domain, NewDomain))
DOMAIN_IN(.(X, Rest), Domain) → SELECT_IN(X, Domain, NewDomain)
SELECT_IN(X, .(Y, R), .(Y, Rest)) → U23¹(X, Y, R, Rest, select_in(X, R, Rest))
SELECT_IN(X, .(Y, R), .(Y, Rest)) → SELECT_IN(X, R, Rest)
U21¹(X, Rest, Domain, select_out(X, Domain, NewDomain)) → U22¹(X, Rest, Domain, domain_in(Rest, NewDomain))
U21¹(X, Rest, Domain, select_out(X, Domain, NewDomain)) → DOMAIN_IN(Rest, NewDomain)
U15¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U15¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → HOUSES_IN(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))
U16¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U16¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → HOUSES_IN(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))
U17¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U17¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → HOUSES_IN(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))
U18¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U18¹(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → HOUSES_IN(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))

The TRS R consists of the following rules:

zebra_in(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in(Englishman, Red))
eq_in(X, X) → eq_out(X, X)
U1(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out(Englishman, Red)) → U2(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in(Spaniard, Dog))
U2(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out(Spaniard, Dog)) → U3(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in(Green, Coffee))
U3(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out(Green, Coffee)) → U4(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in(Ukrainian, Tea))
U4(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out(Ukrainian, Tea)) → U5(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in(Green, Ivory))
to_the_right_in(second, first) → to_the_right_out(second, first)
to_the_right_in(third, second) → to_the_right_out(third, second)
to_the_right_in(fourth, third) → to_the_right_out(fourth, third)
to_the_right_in(fifth, fourth) → to_the_right_out(fifth, fourth)
U5(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out(Green, Ivory)) → U6(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in(Winston, Snails))
U6(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out(Winston, Snails)) → U7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in(Kool, Yellow))
U7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out(Kool, Yellow)) → U8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in(Milk, third))
U8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out(Milk, third)) → U9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in(Norwegian, first))
U9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out(Norwegian, first)) → U10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in(Fox, Chesterfield))
next_to_in(first, second) → next_to_out(first, second)
next_to_in(second, first) → next_to_out(second, first)
next_to_in(second, third) → next_to_out(second, third)
next_to_in(third, second) → next_to_out(third, second)
next_to_in(third, fourth) → next_to_out(third, fourth)
next_to_in(fourth, third) → next_to_out(fourth, third)
next_to_in(fourth, fifth) → next_to_out(fourth, fifth)
next_to_in(fifth, fourth) → next_to_out(fifth, fourth)
U10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out(Fox, Chesterfield)) → U11(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in(Horse, Kool))
U11(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out(Horse, Kool)) → U12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in(Lucky, Juice))
U12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out(Lucky, Juice)) → U13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in(Japanese, Parliament))
U13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out(Japanese, Parliament)) → U14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in(Norwegian, Blue))
U14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out(Norwegian, Blue)) → U15(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in(Prop) → U20(Prop, domain_in(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in(.(X, Rest), Domain) → U21(X, Rest, Domain, select_in(X, Domain, NewDomain))
select_in(X, .(Y, R), .(Y, Rest)) → U23(X, Y, R, Rest, select_in(X, R, Rest))
select_in(X, .(X, R), R) → select_out(X, .(X, R), R)
U23(X, Y, R, Rest, select_out(X, R, Rest)) → select_out(X, .(Y, R), .(Y, Rest))
U21(X, Rest, Domain, select_out(X, Domain, NewDomain)) → U22(X, Rest, Domain, domain_in(Rest, NewDomain))
domain_in([], X) → domain_out([], X)
U22(X, Rest, Domain, domain_out(Rest, NewDomain)) → domain_out(.(X, Rest), Domain)
U20(Prop, domain_out(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out(Prop)
U15(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SELECT_IN(X, .(Y, R), .(Y, Rest)) → SELECT_IN(X, R, Rest)

The TRS R consists of the following rules:

zebra_in(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in(Englishman, Red))
eq_in(X, X) → eq_out(X, X)
U1(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out(Englishman, Red)) → U2(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in(Spaniard, Dog))
U2(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out(Spaniard, Dog)) → U3(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in(Green, Coffee))
U3(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out(Green, Coffee)) → U4(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in(Ukrainian, Tea))
U4(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out(Ukrainian, Tea)) → U5(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in(Green, Ivory))
to_the_right_in(second, first) → to_the_right_out(second, first)
to_the_right_in(third, second) → to_the_right_out(third, second)
to_the_right_in(fourth, third) → to_the_right_out(fourth, third)
to_the_right_in(fifth, fourth) → to_the_right_out(fifth, fourth)
U5(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out(Green, Ivory)) → U6(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in(Winston, Snails))
U6(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out(Winston, Snails)) → U7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in(Kool, Yellow))
U7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out(Kool, Yellow)) → U8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in(Milk, third))
U8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out(Milk, third)) → U9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in(Norwegian, first))
U9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out(Norwegian, first)) → U10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in(Fox, Chesterfield))
next_to_in(first, second) → next_to_out(first, second)
next_to_in(second, first) → next_to_out(second, first)
next_to_in(second, third) → next_to_out(second, third)
next_to_in(third, second) → next_to_out(third, second)
next_to_in(third, fourth) → next_to_out(third, fourth)
next_to_in(fourth, third) → next_to_out(fourth, third)
next_to_in(fourth, fifth) → next_to_out(fourth, fifth)
next_to_in(fifth, fourth) → next_to_out(fifth, fourth)
U10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out(Fox, Chesterfield)) → U11(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in(Horse, Kool))
U11(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out(Horse, Kool)) → U12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in(Lucky, Juice))
U12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out(Lucky, Juice)) → U13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in(Japanese, Parliament))
U13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out(Japanese, Parliament)) → U14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in(Norwegian, Blue))
U14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out(Norwegian, Blue)) → U15(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in(Prop) → U20(Prop, domain_in(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in(.(X, Rest), Domain) → U21(X, Rest, Domain, select_in(X, Domain, NewDomain))
select_in(X, .(Y, R), .(Y, Rest)) → U23(X, Y, R, Rest, select_in(X, R, Rest))
select_in(X, .(X, R), R) → select_out(X, .(X, R), R)
U23(X, Y, R, Rest, select_out(X, R, Rest)) → select_out(X, .(Y, R), .(Y, Rest))
U21(X, Rest, Domain, select_out(X, Domain, NewDomain)) → U22(X, Rest, Domain, domain_in(Rest, NewDomain))
domain_in([], X) → domain_out([], X)
U22(X, Rest, Domain, domain_out(Rest, NewDomain)) → domain_out(.(X, Rest), Domain)
U20(Prop, domain_out(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out(Prop)
U15(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SELECT_IN(X, .(Y, R), .(Y, Rest)) → SELECT_IN(X, R, Rest)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x2)
SELECT_IN(x1, x2, x3) = SELECT_IN(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

SELECT_IN(.(R)) → SELECT_IN(R)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

SELECT_IN(.(R)) → SELECT_IN(R)
The graph contains the following edges 1 > 1

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

DOMAIN_IN(.(X, Rest), Domain) → U21¹(X, Rest, Domain, select_in(X, Domain, NewDomain))
U21¹(X, Rest, Domain, select_out(X, Domain, NewDomain)) → DOMAIN_IN(Rest, NewDomain)

The TRS R consists of the following rules:

zebra_in(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water) → U1(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_in(Englishman, Red))
eq_in(X, X) → eq_out(X, X)
U1(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, eq_out(Englishman, Red)) → U2(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_in(Spaniard, Dog))
U2(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, eq_out(Spaniard, Dog)) → U3(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_in(Green, Coffee))
U3(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, eq_out(Green, Coffee)) → U4(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_in(Ukrainian, Tea))
U4(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, eq_out(Ukrainian, Tea)) → U5(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_in(Green, Ivory))
to_the_right_in(second, first) → to_the_right_out(second, first)
to_the_right_in(third, second) → to_the_right_out(third, second)
to_the_right_in(fourth, third) → to_the_right_out(fourth, third)
to_the_right_in(fifth, fourth) → to_the_right_out(fifth, fourth)
U5(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, to_the_right_out(Green, Ivory)) → U6(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_in(Winston, Snails))
U6(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, eq_out(Winston, Snails)) → U7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_in(Kool, Yellow))
U7(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, eq_out(Kool, Yellow)) → U8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_in(Milk, third))
U8(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, eq_out(Milk, third)) → U9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_in(Norwegian, first))
U9(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, eq_out(Norwegian, first)) → U10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_in(Fox, Chesterfield))
next_to_in(first, second) → next_to_out(first, second)
next_to_in(second, first) → next_to_out(second, first)
next_to_in(second, third) → next_to_out(second, third)
next_to_in(third, second) → next_to_out(third, second)
next_to_in(third, fourth) → next_to_out(third, fourth)
next_to_in(fourth, third) → next_to_out(fourth, third)
next_to_in(fourth, fifth) → next_to_out(fourth, fifth)
next_to_in(fifth, fourth) → next_to_out(fifth, fourth)
U10(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, next_to_out(Fox, Chesterfield)) → U11(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_in(Horse, Kool))
U11(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, next_to_out(Horse, Kool)) → U12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_in(Lucky, Juice))
U12(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, eq_out(Lucky, Juice)) → U13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_in(Japanese, Parliament))
U13(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, eq_out(Japanese, Parliament)) → U14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_in(Norwegian, Blue))
U14(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Red, Dog, Green, Coffee, Tea, Ivory, Winston, Snails, Kool, Yellow, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, next_to_out(Norwegian, Blue)) → U15(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, [])))))))
houses_in(Prop) → U20(Prop, domain_in(Prop, .(first, .(second, .(third, .(fourth, .(fifth, [])))))))
domain_in(.(X, Rest), Domain) → U21(X, Rest, Domain, select_in(X, Domain, NewDomain))
select_in(X, .(Y, R), .(Y, Rest)) → U23(X, Y, R, Rest, select_in(X, R, Rest))
select_in(X, .(X, R), R) → select_out(X, .(X, R), R)
U23(X, Y, R, Rest, select_out(X, R, Rest)) → select_out(X, .(Y, R), .(Y, Rest))
U21(X, Rest, Domain, select_out(X, Domain, NewDomain)) → U22(X, Rest, Domain, domain_in(Rest, NewDomain))
domain_in([], X) → domain_out([], X)
U22(X, Rest, Domain, domain_out(Rest, NewDomain)) → domain_out(.(X, Rest), Domain)
U20(Prop, domain_out(Prop, .(first, .(second, .(third, .(fourth, .(fifth, []))))))) → houses_out(Prop)
U15(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Blue, .(Green, .(Red, .(Yellow, .(Ivory, []))))))) → U16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_in(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, [])))))))
U16(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Dog, Coffee, Tea, Winston, Snails, Kool, Milk, Fox, Chesterfield, Horse, Lucky, Juice, Parliament, houses_out(.(Norwegian, .(Englishman, .(Spaniard, .(Japanese, .(Ukrainian, []))))))) → U17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_in(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, [])))))))
U17(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Winston, Kool, Milk, Chesterfield, Lucky, Juice, Parliament, houses_out(.(Dog, .(Zebra, .(Fox, .(Snails, .(Horse, []))))))) → U18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_in(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, [])))))))
U18(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, Coffee, Tea, Milk, Juice, houses_out(.(Parliament, .(Kool, .(Lucky, .(Chesterfield, .(Winston, []))))))) → U19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_in(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, [])))))))
U19(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water, houses_out(.(Milk, .(Juice, .(Water, .(Tea, .(Coffee, []))))))) → zebra_out(Englishman, Spaniard, Japanese, Ukrainian, Norwegian, Zebra, Water)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

DOMAIN_IN(.(X, Rest), Domain) → U21¹(X, Rest, Domain, select_in(X, Domain, NewDomain))
U21¹(X, Rest, Domain, select_out(X, Domain, NewDomain)) → DOMAIN_IN(Rest, NewDomain)

The TRS R consists of the following rules:

select_in(X, .(Y, R), .(Y, Rest)) → U23(X, Y, R, Rest, select_in(X, R, Rest))
select_in(X, .(X, R), R) → select_out(X, .(X, R), R)
U23(X, Y, R, Rest, select_out(X, R, Rest)) → select_out(X, .(Y, R), .(Y, Rest))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x2)
select_in(x1, x2, x3) = select_in(x2)
U23(x1, x2, x3, x4, x5) = U23(x5)
select_out(x1, x2, x3) = select_out(x3)
DOMAIN_IN(x1, x2) = DOMAIN_IN(x1, x2)
U21¹(x1, x2, x3, x4) = U21¹(x2, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

DOMAIN_IN(.(Rest), Domain) → U21¹(Rest, select_in(Domain))
U21¹(Rest, select_out(NewDomain)) → DOMAIN_IN(Rest, NewDomain)

The TRS R consists of the following rules:

select_in(.(R)) → U23(select_in(R))
select_in(.(R)) → select_out(R)
U23(select_out(Rest)) → select_out(.(Rest))

The set Q consists of the following terms:

select_in(x0)
U23(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

U21¹(Rest, select_out(NewDomain)) → DOMAIN_IN(Rest, NewDomain)
The graph contains the following edges 1 >= 1, 2 > 2
DOMAIN_IN(.(Rest), Domain) → U21¹(Rest, select_in(Domain))
The graph contains the following edges 1 > 1